#include "PDTExpNumBin.h"
#include "PDTCodeGraph.h"
#include "PDTZ3GraphVisitor.h"

PDTExpNumBin::PDTExpNumBin(PDTCodeGraph & CG):PDTExpNum(CG){
	//maybe intialize to some value
}

void PDTExpNumBin::setLeft(PDTExpNum&left){
	addChild(&left);
	left.addParent(this);
}
void PDTExpNumBin::setRight(PDTExpNum &right){
	addChild(&right);
	right.addParent(this);
}


PDTExpNumBin::PDTExpNumBin(PDTCodeGraph & CG,PDTExpNum &left,PDTExpNum & right):PDTExpNum(CG){
	addChild(&left);
	left.addParent(this);


	addChild(&right);
	right.addParent(this);

}

PDTExpNum * PDTExpNumBin::getLeft(){
	return dynamic_cast<PDTExpNum*>(children[0]);
}

PDTExpNum * PDTExpNumBin::getRight(){
	return dynamic_cast<PDTExpNum*>(children[1]);
}

void
PDTExpNumBin::Z3NodeVisitHelper(PDTZ3Visitor & ZV, Z3_ast * args)
{
    //Z3_ast child1 = getLeft()->Z3visit(ZV);
    //Z3_ast child2 = getRight()->Z3visit(ZV);

    //args[0] =  getLeft()->Z3value(ZV);
    //args[1] = getRight()->Z3value(ZV);

    assert(Z3_get_sort(ZV.ctx, args[0]) == Z3_get_sort(ZV.ctx, args[1]));
    assert(Z3_get_sort(ZV.ctx, args[0]) == ZV.Int);
}

